Nuprl Definition : ring_hom 13,42
RingHom(R;S)
== {f:|R||S|| FunThru2op(|R|;|S|;+R;+S;f) & FunThru2op(|R|;|S|;*;*;f) & f(1) = 1}  
latex

clarification:

RingHom(R;S)
== {f:|R||S|| 
== {FunThru2op(|R|;|S|;+R;+S;f) & FunThru2op(|R|;|S|;*R;*S;f) & f(1R) = (1S)  |S|}  
latex

Uprings 1
Wellformedness Lemmasring hom wf
Definitions+r, P & Q, FunThru2op(A;B;opa;opb;f), *, |r|, 1

origin